Inference at * 
Iof proof for Lemma p-fun-exp-add1-sq:


  A:Type, f:(A(A + Top)), x:A, n:.
  (can-apply(f;x))  ((f^n+1(x)) ~ (f^n(do-apply(f;x)))) 

latex

 by (Unfolds ``can-apply do-apply`` ( 0)) 
CollapseTHEN ((UnivCD) 
CollapseTHENA (Auto))
C 

latex

C1: 

C1: 1. A : Type
C1: 2. f : A(A + Top)
C1: 3. x : A
C1: 4. n : 
C1: 5. isl(f(x))
C1:   (f^n+1(x)) ~ (f^n(outl(f(x))))
C.

Definitions	can-apply(f;x), do-apply(f;x), P  Q, b, isl(x), x:A. B(x), f(a), , x:AB(x), left + right, Top, t  T, Type
Lemmas	assert wf, isl wf, nat wf, top wf